
\documentclass[12pt,a4paper]{report}
\usepackage{ifpdf}
\usepackage[utf8]{inputenc}
\usepackage[francais]{babel}
\usepackage[T1]{fontenc}
\usepackage[unicode=true,pdftex,colorlinks=true,linkcolor=black,urlcolor=black,
  citecolor=black]{hyperref}
\usepackage{natbib}
\usepackage{graphicx}

%\parindent 0.6cm
%\setlength{\parskip}{0.5em plus 0.2em minus 0.2em}

\title{Rapport Projet Construction formelle}
\author{Frédéric \textsc{Bouvet} \and  Hervé \textsc{Esteguet}  \and Laurent \textsc{Maillet}}
\date{\today}
\ifpdf
\pdfinfo{
/Author (Frédéric Bouvet Laurent Maillet Hervé
Esteguet)
/Title (Rapport Projet construction formelle)
/Subject (Rapport Projet construction formelle)
/Keywords (Event-B, SOAP)
/CreationDate (D:20100329212218)
}
\fi

\newcommand{\HRule}{\rule{\linewidth}{0.5mm}}
\newcommand{\emphbf}[1]{\textbf{\emph{#1}}}

\begin{document}

%% Puces au lieu de tirets dans les listes:
\renewcommand{\labelitemi}{\textbullet}
\renewcommand{\labelitemii}{\textbullet}
\renewcommand{\labelitemiii}{\textbullet}

\input{title.tex}

\clearpage
\tableofcontents
\clearpage

\begin{abstract}
Les interactions entre services réparti sur les réseaux internet utilisent entre autre le protocole SOAP. Pour étudier ces interactions, un modèle des services et des protocoles qu'ils utilisent est nécessaire. C'est ce à quoi s'attache ce projet, réalisé dans le cadre du module "construction formelle" du Master 2 ALMA.
Dans un premier temps nous parlerons de la méthode B et du B événementiel, puis nous détaillerons l'analyse, la spécification et le développement de notre modèle. Enfin nous donnerons le planning de suivi avant de conclure. 
\end{abstract}


\chapter{Introduction}
La méthode B est une méthode formelle de développement logiciel qui permet de modéliser de façon abstraite dans le langage de B le comportement d'un programme, puis par raffinements successifs, d'aboutir à un modèle concret, sous-ensemble du langage transcodable en Ada ou en C.
Une activité de preuve formelle permet de vérifier la cohérence du modèle abstrait et la conformité de chaque raffinement avec le modèle supérieur (prouvant ainsi la conformité de l'ensemble des implémentations concrètes avec le modèle abstrait).
On distingue le:
\begin{itemize}
 \item B classique tel qu'il est défini dans le B Book de 1996. L'outil logiciel de support est l'atelier B, ou le B-Toolkit.
 \item B événementiel qui est une évolution utilisant uniquement la notion d'événements pour décrire les actions et non plus les opérations.
\end{itemize}

Le modèle que nous présentons a été réalisé en B événementiel (Event-B).

\chapter{Analyse}
\section{D\'efinitions des concepts}
En partants des concepts de messages et services, on déduit qu'il va s'agir d'un graphe dont les nœuds sont des services. Ces nœuds doivent pouvoir communiquer entre eux (s'envoyer des messages).
\subsection{Services}
\subsubsection{Voisin}
Pour relié les services entre eux (ce qui représente les arrêtes du graphe), nous avons besoin de la notion de voisin: Cela permettra à un service de savoir quels autres services lui sont directement accessible.
\subsubsection{Accessible}
On aimerait également pouvoir communiquer avec des services plus lointains, pour cela il nous faut connaître quels sont les services accessibles indirectement (par saut successif), on introduit donc la notion d'accessibilité.
\subsection{Messages}
\subsubsection{Destinataire}
Pour un message, on a classiquement un destinataire et un expéditeur (qui sont des services). Comme les messages peuvent transiter entre plusieurs services avant d'arriver à destination, la notion d'expéditeur étant trop vague dans notre cas, elle doit être précisé (car un même message est expédié plusieurs fois par des services différents avant d'arriver à son objectif): 
\subsubsection{cr\'eateur et origine}
on a donc un créateur (le service qui a créé et envoyé le message pour la première fois) et une origine (qui changera à chaque "saut"). Nous pourrions garder en mémoire le chemin entier pris par le message (donc avoir une liste de services d'origine), mais la traçabilité complète n'est pas particulièrement utile dans le cadre de ce projet.

\begin{figure}[h!]
 \centering
 \includegraphics[width=\textwidth]{images/diag1.jpg}
 \caption{exemple des concepts pr\'esent\'e: on a un service 1 qui a pour voisin 2. Le 2 \'etant voisin a 4, le service 1 peut acc\'eder au 4}
\end{figure}


\chapter{Spécification}
\section{Ensembles}
On prend deux ensembles: MESSAGE et SERVICE, qui définissent respectivement l'ensemble des messages et des services.
\section{Relations}
Une relation binaire entre deux ensemble A et B est un sous-ensemble du produit cart\'esien AxB.
Dans notre mod\`ele nous avons diff\'erentes relations:
\begin{itemize}
 \item neighbor: SERVICE <-> SERVICE \textit{permet a un service de connaitre l'ensemble de ses voisins}
 \item accessible: SERVICE <-> SERVICE \textit{permet a un service de connaitre l'ensemble des SERVICE qu'il peut atteindre}
 \item received: SERVICE <-> messages \textit{contient l'ensemble des messages envoyes et arrives a bonne destination}
 \item receivedButNotForMe: SERVICE <-> \textit{messages contient l'ensemble des messages envoyes et n'etant pas encore arrives a bonne destination}
\end{itemize}
\section{Fonctions partielles}
Une fonction partielle sur un ensemble donné E est une fonction définie sur une partie de celui-ci, qui est alors appelé domaine de définition de la fonction partielle.
Dans notre mod\`ele, on a les fonctions partielles suivantes (messages est un sous-ensemble de MESSAGE):
\begin{itemize}
 \item Origin: messages +-> SERVICE \textit{definit l'origine d'un message}
 \item Destination: messages +-> SERVICE \textit{definit le destinataire d'un message}
 \item Creator: messages +-> SERVICE \textit{definit le createur d'un message et donc sa reel origine}
\end{itemize}

\section{\'Ev\'enement}
Pour un service pr\'ecis une r\'eception de message n'est pas une op\'eration mais un \'evenement, nous avons donc sp\'ecifier notre mod\`ele en Event-B car cel\`a permet la gestion des \'ev\'enements.
   
\subsection{Cr\'eation d'un message}
\subsubsection{Param\`etres}
Pour cr\'eer un messages il nous faut un service d'origine src et un de destination dst et que dst soit accessible \`a partir de src.
\subsubsection{Action}
On ajoute un message a l'ensemble MESSAGE, on indique que ce message a pour origine et createur src, ainsi que dst comme destination.
 
\subsection{Premier envoi du message}
\subsubsection{Param\`etres}
On a besoin de savoir quel message envoyer.
\subsubsection{Action}
Envoie du message et on sp\'ecifie que la nouvelle origine du message.
    
\subsection{Envoi d'un message recu mais dont je ne suis pas le destinataire}
\subsubsection{Param\`etres}
Il nous faut le message a envoyer et le service qui sera le prochain noeud a recevoir le message.
\subsubsection{Action}
On met \`a jour l'origine du message et on enleve le message de l'ensemble de ceux qui \'etais re\c{c}u dont je ne suis pas le destinataire.

\subsection{Reception d'un message dont je ne suis pas le destinataire}
\subsubsection{Param\`etres}
Le message re\c{c}u.
\subsubsection{Action}  
On ajoute le message re\c{c}u a l'ensemble de ceux qui \'etais re\c{c}u dont je ne suis pas le destinataire.
    
\subsection{Reception d'un message dont je suis le destinataire}
\subsubsection{Param\`etres}
Le message re\c{c}u.
\subsubsection{Action} 
On ajoute le message a l'ensemble des messages re\c{c}u et on l'enleve de l'ensemble des envois.

\chapter{Planning de suivi (Gantt)}
\begin{figure}[h!]
 \centering
 \includegraphics[width=\textwidth]{images/gantt.jpg}
 \caption{Diagramme de Gantt}
\end{figure}

\chapter{Conclusion}
Ce projet nous a permis de concevoir un modèle et de le spécifier en Event-B. Nous avons pu découvrir différents outils autour d'Event-B, notamment Rodin et Pro-B. 
Rodin est un environnement de développement dédié à l'Event-B, nous avons malheureusement rencontré des difficultés à le faire fonctionner. En revanche, Pro-B s'est avérer être un outil particulièrement utile pour simuler le fonctionnement du modèle, générer les preuves et vérifier la cohérence du modèle. Nous avions également voulu procéder à l'élaboration d'un raffinement du modèle, cependant il n'y avais rien de particulièrement utile à raffiner.
Notre travail modélise bien un réseau de communication de type SOAP, il peut servir de bases pour ajouter différentes spécifications techniques relatives au protocole SOAP (contenu des messages, ports, binding...)

\end{document}
